es:ES, l:IdLnk, tgs:Id List, da:k:Knd fp Type, ds:x:Id fp Type,
f:(z:((e':E. isrcv(e')  lnk(e') = l  (tag(e')  tgs)  valtype(e')  da(kind(e'))?Void)
f:(z:(& (x:Id. vartype(source(l);x)  ds(x)?Top)).
f:({e:E| loc(e) = source(l)  Id }((tg:Idda(rcv(l,tg))?Void) List)).
with decls ds dasends on l from e include f(e) and only these for tags in tgs  Prop 

latex

Definitions

t  T, P  Q, x:A. B(x), tag(e), ||as||, index(e), E, b, IdLnk, s = t, Id, (x  l), x:AB(x), P & Q, A & B, x:A. B(x), True, Void, Type, kind(e), rcv(l,tg), <a,b>, Knd, KindDeq, x.A(x), x. t(x), T, x:AB(x), f(a), x(s), a:A fp B(a), EqDecider(T), f(x)?z, valtype(e), val(e), P  Q, P  Q, source(l), loc(e), False, A, ES, type List, x:A. B(x), e@i. P(e), A/x,y. B(x;y), 1of(t), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, a<b, {T}, SQType(T), Prop, s ~ t, destination(l), sender(e), {x:A| B(x) }, ij, sends(l;e), (Msg on l), #$n, {i..j}, l[i], AB, , lnk(e), isrcv(e), i  j < k, Top, IdDeq, vartype(i;x), with decls ds dasends on l from e include f(e) and only these for tags in tgs

Lemmas

event system wf, es-kind wf, es-vartype wf, id-deq wf, top wf, alle-at wf, es-E wf, assert wf, es-isrcv wf, es-lnk wf, l member wf, subtype rel self, select wf, non neg length, int seg wf, length wf1, es-Msgl wf, es-sends wf, rcv wf, es-index wf, es-loc wf, es-sender wf, lsrc wf, ldst wf, IdLnk wf, IdLnk sq, es-loc-pred, es-loc-sender, Id wf, es-val wf, subtype rel wf, es-valtype wf, fpf-cap wf, squash wf, true wf, deq wf, fpf wf, Knd wf, Kind-deq wf, es-rcv-kind, es-tag wf